(declare-const v1 Bool)
(declare-const v5 Bool)
(declare-const v7 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const v19 Bool)
(declare-const r3 Real)
(declare-const _22-0 (_ BitVec 22))
(declare-const r4 Real)
(declare-const v20 Bool)
(assert (not (exists ((q2 Real) (q3 (_ BitVec 12)) (q4 Int) (q5 (_ BitVec 10))) (or v12 v7 (xor (bvsge _22-0 _22-0) v13 v20 v15 v16 (< r2 (* 0.9852344103 0.9852344103 r2 0.9852344103 r4) 0.9852344103 r3 r0) v5 v10 v20) (xor (bvsge _22-0 _22-0) v13 v20 v15 v16 (< r2 (* 0.9852344103 0.9852344103 r2 0.9852344103 r4) 0.9852344103 r3 r0) v5 v10 v20)))))
(check-sat)
